COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.device xgp
C00005 ENDMK
C⊗;
.device xgp
.font 1 "baxl30" <<text>>
.font 2 "bdr30" <<sym>>
.font 3 "baxm30" <<var>>
.sides←1
.require "twocol.pub[sub,sys]" source_file
.require"lispub.pub[206,lsp]"source
.turn on "→∂{"
.onecol
.macro sho(v)	⊂tty←"v: "&v;⊃
.s PROVING LISP PROGRAMS CORRECT

	In this chapter we will introduce techniques for proving
LISP programs correct.
The techniques will mainly be limited to what we may call %3clean%1
LISP programs.  In particular, there must be no side effects,
because our methods depend on the ability to replace subexpressions
by equal expressions.

.ss Proofs by structural induction.

	Recall that the operation of appending two lists is defined by

!!si2:	%3x * y ← %4if n%3 x %4then%3 y %4else a%3 x . [%4d%3 x * y]%1.

Because %3x*y%1 is defined for all %3x%1 and %3y%1, i.e. the computation
described above terminates for all %3x%1 and %3y%1, we can replace ({[5] si2})
by the sentence

!!si1:	%3∀x y:[islist x ∧ islist y ⊃
[%3x * y = %4if n%3 x %4then%3 y %4else a%3 x . [%4d%3 x * y]]]%1.

Now suppose we would like to prove %3∀y:[%5NIL%3 * y = y]%1.  This is
quite trivial; we need only substitute %5NIL%1 for %3x%1 in ({[5] si1}),
getting

→%5NIL%3 * y ∂(15) = %4if n %5NIL %4then%3 y %4else a %5NIL%3 . [%4d %5NIL%3 * y]

∂(15) = y%1.

Next consider proving %3∀x:[x * %5NIL%3 = x]%1.  This cannot be done by
simple substitution, but it can be done as follows:  First substitute
%3λx:[x * %5NIL%3 = x]%1 for %3P%1 in the induction schema

	%3∀u:[islist u ⊃ [%4n%3 u ∨ P[%4d%3 u] ⊃ P[u]]] ⊃ ∀u:[islist u
⊃ P[u]]%1,

getting

	%3∀u:[islist u ⊃ [%4n%3 u ∨ %3λx:[x * %5NIL%3 = x][%4d%3 u]
⊃ %3λx:[x * %5NIL%3 = x][u]]] ⊃ ∀u:[islist u
⊃ %3λx:[x * %5NIL%3 = x][u]]%1.

Carrying out the indicated lambda conversions makes this

	%3∀u:[islist u ⊃ [%4n%3 u ∨ %4d%3 u * %5NIL%3 = %4d%3 u]
⊃ u * %5NIL%3 = u] ⊃ ∀u:[islist u ⊃ u * %5NIL%3 = u]%1.